;; Copyright © 2016, cage
;; All rights reserved.

;; Redistribution and use in source and binary forms, with or without
;; modification, are permitted provided that the following conditions are met:

;;     * Redistributions of source code must retain the above copyright
;; notice, this list of conditions and the following disclaimer.
;;     * Redistributions in binary form must reproduce the above copyright
;; notice, this list of conditions and the following disclaimer in the
;; documentation and/or other materials provided with the distribution.

;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
;; AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
;; LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
;; CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
;; SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
;; CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
;; ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
;; THE POSSIBILITY OF SUCH DAMAGE.

(in-package :mini-kanren)

(defmacro project ((&rest vars) &body goals)
  (with-gensyms (subst)
    (let* ((let-clauses (loop for v in vars collect
			     `(,v (walk* ,v (car ,subst))))))
      `#'(lambda (,subst)
	   (let ,let-clauses
	     (declare (ignorable ,@vars))
	     (funcall (all ,@goals) ,subst))))))

(defmacro ifte* (gs &optional (hs nil) &body body)
  (if  (null hs)
      `(conj-plus ,gs)
      `(ifte ,(first gs)
	     (conj-plus ,@(rest gs))
	     (ifte*     (,@hs) ,@body))))

(defmacro conda ((&rest gs) (&rest hs) &body body)
  `(symbol-macrolet ((else +succeed+))
     (zzz (ifte* (,@gs +succeed+) (,@hs +succeed+) ,@body +fail+))))

(defmacro condu ((&rest gs) (&rest hs) &body body)
  `(conda ((once ,(first gs)) ,@(rest gs))
       ((once ,(first hs)) ,@(rest hs))
     ,@body))

(defmacro condi (&rest clauses)
  `(conde ,@clauses))

(defun ==-check (v w)
  (== v w))

(defmacro all-aux (bnd &rest goals)
  (cond ((null goals)
         '+succeed+)
        ((null (cdr goals))
         (car goals))
        (t
	 (with-gensyms (goal all-aux-subst)
	   (let ((remaining-goals (cdr goals)))
	     `(let ((,goal ,(car goals)))
		(lambda-g (,all-aux-subst)
		  (funcall ,bnd
			   (funcall ,goal ,all-aux-subst)
			   (lambda-g (,all-aux-subst)
			     (funcall (all-aux ,bnd ,@remaining-goals)
				      ,all-aux-subst))))))))))

(defun mplusi ($1 $2)
  (cond
    ((null $1)
     $2)
    ((functionp $1)
     (lambda-$ () (mplus $2 (funcall $1))))
    (t
     (cons (car $1)
	   (mplusi $1 (cdr $2))))))

(defun bindi ($ g)
  (cond
    ((null $)
     +mzero+)
    ((functionp $)
     (lambda-$ () (bind (funcall $) g)))
    (t
     (mplusi (funcall g (car $))
	    (bindi (cdr $) g)))))


(defmacro all (&rest goals)
  `(all-aux #'bind ,@goals))

(defmacro alli (&rest goals)
  `(all-aux #'bindi ,@goals))

;; The absolute basics
(defun nullo (object)
  (== '() object))

(defun conso (car cdr cons)
  (== (cons car cdr) cons))

;; Conso intermediates
;;; You can do any of these with raw conso, but naming them makes things clearer.
(defun caro (cons car)
  (fresh (cdr) (== (cons car cdr) cons)))

(defun cdro (cons cdr)
  (fresh (car) (== (cons car cdr) cons)))

(defun pairo (pair?)
  (fresh (car cdr) (conso car cdr pair?)))

(defun eq-caro (list x)
  (caro list x))

;; Some list primitives
(defun listo (list)
  (conde ((nullo list) +succeed+)
         ((pairo list)
          (fresh (d)
            (cdro list d)
            (listo d)))
         (else +fail+)))

(defun membero (x list)
  (conde ((nullo list) +fail+)
         ((eq-caro list x) +succeed+)
         (else (fresh (d)
                 (cdro list d)
                 (membero x d)))))

(defun appendo (list rest out)
  (conde ((nullo list) (== rest out))
         (else (fresh (a d result)
                 (conso a d list)
                 (conso a result out)
                 (appendo d rest result)))))

(defun secondo (cons-cell out)
  (fresh (d)
    (cdro cons-cell d)
    (caro d out)))

(defun thirdo (cons-cell out)
  (fresh (c d d2)
    (cdro cons-cell d)
    (cdro d d2)
    (caro d2 out)))

;; Some tree primitives
(defun brancho (x tree)
  (fresh (car cdr)
    (conso car cdr tree)
    (conde ((nullo tree) +fail+)
	   ((== car x) +succeed+)
	   ((brancho x car))
	   (else (brancho x cdr)))))

(defun flatteno (list? out)
  (conde ((nullo list?) (== '() out))
         ((pairo list?)
          (fresh (a d result-car result-cdr)
            (conso a d list?)
            (flatteno a result-car)
            (flatteno d result-cdr)
            (appendo result-car result-cdr out)))
         (else (conso list? '() out))))

(defmacro choice-case (key-term &body cases)
  (let ((kt-name (gensym)))
    `(fresh (,kt-name)
       (== ,key-term ,kt-name)
       (conde ,@(mapcar (lambda (case)
                          (destructuring-bind (keys &rest clauses) case
                            (cond ((eql keys 'else)
                                   clauses)
                                  ((consp keys)
                                   (if (cdr keys)
                                       `((conde ,@(mapcar (lambda (key)
                                                        `(== ,kt-name ',key))
                                                      keys))
                                         ,@clauses)
                                       `((== ,kt-name ',(car keys))
                                         ,@clauses)))
                                  (t `((== ,kt-name ',keys)
                                       ,@clauses)))))
                        cases)))))

(defun map-choice (fun &rest bindings)
  (labels ((compose-bindings (relation bindings)
             (if (some #'null bindings)
                 relation
                 (let ((terms (mapcar #'car bindings)))
                   (compose-bindings (conde (relation)
                                            ((apply fun terms)))
                                     (mapcar #'cdr bindings))))))
    (compose-bindings +fail+ bindings)))

(defun permute-binary-relation (relation)
  (lambda (a b)
    (conde ((funcall relation a b))
           ((funcall relation b a)))))

(defun make-binary-relation (mapping)
  (lambda (a b)
    (map-choice (lambda (a1 b1)
                  (fresh ()
                    (== a a1)
                    (== b b1)))
                (mapcar #'first mapping)
                (mapcar #'second mapping))))

;;this needs to confirm that compile time evaluation is possible:
;;mapping is a quoted list, n is a number, etc
#+ (or)
(define-compiler-macro make-nary-relation (n mapping)
  (let* ((maps (loop :for x :from 0 :below n
                  :collect `',(mapcar (lambda (list)
                                     (nth x list))
                                   mapping)))
         (args (loop :for x :from 0 :below n
                  :collect (gensym)))
         (args1 (loop :for x :from 0 :below n
                   :collect (gensym)))
         (sequence (mapcar (lambda (a a1)
                             `(== ,a ,a1))
                           args
                           args1)))
    `(lambda ,args
       (map-choice (lambda ,args1
                     (fresh ()
                       ,@sequence))
                   ,@maps))))

(defun make-nary-relation (n mapping)
  (let ((maps (loop :for x :from 0 :below n
                 :collect (mapcar (lambda (list)
                                    (nth x list))
                                  mapping))))
    (lambda (&rest args)
      (unless (= (length args) n)
        (error "invalid number of arguments"))
      (apply #'map-choice
             (lambda (&rest args1)
               (let ((sequence nil))
                 (map nil (lambda (a a1)
                            (unless sequence
                              (setf sequence (== a a1)))
                            ;; we don't want to capture the binding
                            ;; (this should be a fold)
                            (let ((seq sequence))
                              (setf sequence (fresh () seq (== a a1)))))
                      args
                      args1)
                 sequence))
             maps))))

(defun permute-ternary-relation (relation)
  (lambda (a b c)
    (conde ((funcall relation a b c))
           ((funcall relation a c b))
           ((funcall relation c b a))
           ((funcall relation b a c))
           ((funcall relation c a b))
           ((funcall relation b c a)))))

(defun make-ternary-relation (mapping)
  (lambda (a b c)
    (map-choice (lambda (a1 b1 c1)
                  (fresh ()
                    (== a a1)
                    (== b b1)
                    (== c c1)))
                (mapcar #'first mapping)
                (mapcar #'second mapping)
                (mapcar #'third mapping))))
